<html>
<head><meta charset="utf-8"><title>symbolic execution · wg-secure-code · Zulip Chat Archive</title></head>
<h2>Stream: <a href="https://rust-lang.github.io/zulip_archive/stream/146229-wg-secure-code/index.html">wg-secure-code</a></h2>
<h3>Topic: <a href="https://rust-lang.github.io/zulip_archive/stream/146229-wg-secure-code/topic/symbolic.20execution.html">symbolic execution</a></h3>

<hr>

<base href="https://rust-lang.zulipchat.com">

<head><link href="https://rust-lang.github.io/zulip_archive/style.css" rel="stylesheet"></head>

<a name="212939432"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/146229-wg-secure-code/topic/symbolic%20execution/near/212939432" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> Shnatsel <a href="https://rust-lang.github.io/zulip_archive/stream/146229-wg-secure-code/topic/symbolic.20execution.html#212939432">(Oct 10 2020 at 23:21)</a>:</h4>
<p>Galois has released a new symbolic execution tool for C, C++ and Rust: <a href="https://crux.galois.com/">https://crux.galois.com/</a><br>
I'm not sure how complete it is, but it does look interesting. I don't think we had any symbolic execution tools Actually Working prior to this.</p>



<a name="212939863"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/146229-wg-secure-code/topic/symbolic%20execution/near/212939863" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> Shnatsel <a href="https://rust-lang.github.io/zulip_archive/stream/146229-wg-secure-code/topic/symbolic.20execution.html#212939863">(Oct 10 2020 at 23:34)</a>:</h4>
<p>I've added it to <a href="https://github.com/rust-secure-code/projects">https://github.com/rust-secure-code/projects</a></p>



<a name="212940937"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/146229-wg-secure-code/topic/symbolic%20execution/near/212940937" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> Joshua Nelson <a href="https://rust-lang.github.io/zulip_archive/stream/146229-wg-secure-code/topic/symbolic.20execution.html#212940937">(Oct 11 2020 at 00:11)</a>:</h4>
<p>Klee would work if you spent enough time messing with it</p>



<a name="212940941"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/146229-wg-secure-code/topic/symbolic%20execution/near/212940941" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> Joshua Nelson <a href="https://rust-lang.github.io/zulip_archive/stream/146229-wg-secure-code/topic/symbolic.20execution.html#212940941">(Oct 11 2020 at 00:11)</a>:</h4>
<p>But it wasn't particularly easy to use</p>



<a name="212974098"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/146229-wg-secure-code/topic/symbolic%20execution/near/212974098" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> Vytautas Astrauskas [he/him] <a href="https://rust-lang.github.io/zulip_archive/stream/146229-wg-secure-code/topic/symbolic.20execution.html#212974098">(Oct 11 2020 at 17:35)</a>:</h4>
<p>If I am not mistaken, <span class="user-mention" data-user-id="336739">@Alastair Reid</span> team is working on having a common interface for Crux, Klee, and Proptest.</p>



<a name="212975132"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/146229-wg-secure-code/topic/symbolic%20execution/near/212975132" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> Alastair Reid <a href="https://rust-lang.github.io/zulip_archive/stream/146229-wg-secure-code/topic/symbolic.20execution.html#212975132">(Oct 11 2020 at 18:01)</a>:</h4>
<p>Yes, our goal is to get as many different tools and as many different <em>types</em> of tool to support a common interface so that:</p>
<p>1) We can switch between symbolic execution, bounded model checking, model checking, abstract interpretation and any other form of verification you wish to use. So you can use the type of tool that best suits the current phase of development.</p>
<p>2) We can switch tools easily. Because even tools of the same type have different sweet spots.</p>
<p>We are building on a foundation of fuzzing and testing (i.e., proptest) because our focus is on how to get orders of magnitude more programmers to use formal verification tools. So we are "meeting developers where they are". That is, we are starting with what programmers are already comfortable with, have experience of, etc. and seeing how far we can get from there.</p>
<p>We are  in a really early stage of this work but you can get what we have here: <a href="https://github.com/project-oak/rust-verification-tools">https://github.com/project-oak/rust-verification-tools</a><br>
At the moment, we have support for KLEE and Crux and we are working to expand that. But, let me warn you that the KLEE setup is painful and and we need to rework the Crux setup to take advantage of the packages in Galois' release.  Very much a work in progress!<br>
If anybody has any other verification tools that work with Rust, we would welcome pull requests, etc.</p>



<a name="213156039"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/146229-wg-secure-code/topic/symbolic%20execution/near/213156039" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> Shnatsel <a href="https://rust-lang.github.io/zulip_archive/stream/146229-wg-secure-code/topic/symbolic.20execution.html#213156039">(Oct 13 2020 at 13:47)</a>:</h4>
<p>perhaps <a href="https://github.com/viperproject/prusti-dev/">https://github.com/viperproject/prusti-dev/</a> but the setup is also a pain, and it requires a vastly outdated version of rustc</p>



<a name="213161971"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/146229-wg-secure-code/topic/symbolic%20execution/near/213161971" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> Vytautas Astrauskas [he/him] <a href="https://rust-lang.github.io/zulip_archive/stream/146229-wg-secure-code/topic/symbolic.20execution.html#213161971">(Oct 13 2020 at 14:24)</a>:</h4>
<p><span class="user-mention silent" data-user-id="127617">Shnatsel</span> <a href="#narrow/stream/146229-wg-secure-code/topic/symbolic.20execution/near/213156039">said</a>:</p>
<blockquote>
<p>perhaps <a href="https://github.com/viperproject/prusti-dev/">https://github.com/viperproject/prusti-dev/</a> but the setup is also a pain, and it requires a vastly outdated version of rustc</p>
</blockquote>
<p>We are currently switching to the latest version of Rustc, so some setup things and documentation could be temporarily broken. However, if you have problems getting started with the <a href="https://marketplace.visualstudio.com/items?itemName=viper-admin.prusti-assistant">VS Code extension</a>, we would appreciate a bug report <span aria-label="smiling face" class="emoji emoji-263a" role="img" title="smiling face">:smiling_face:</span>.</p>



<a name="213163750"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/146229-wg-secure-code/topic/symbolic%20execution/near/213163750" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> Shnatsel <a href="https://rust-lang.github.io/zulip_archive/stream/146229-wg-secure-code/topic/symbolic.20execution.html#213163750">(Oct 13 2020 at 14:34)</a>:</h4>
<p>Oh, I wasn't aware of the extension! That looks like it simplifies things a lot, thanks!</p>



<a name="213341722"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/146229-wg-secure-code/topic/symbolic%20execution/near/213341722" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> nyms <a href="https://rust-lang.github.io/zulip_archive/stream/146229-wg-secure-code/topic/symbolic.20execution.html#213341722">(Oct 14 2020 at 19:47)</a>:</h4>
<p>hi all, I'm working on the beginning stages of adding <a href="https://github.com/eurecom-s3/symcc">https://github.com/eurecom-s3/symcc</a> as an LLVM codegen pass. I saw some questions in #general and #t-compiler/help about passes, and going to try out some hacks with <code>cc</code> and backend <code>rustc</code> stuff. open to any pointers and/or collaboration</p>



<a name="216345324"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/146229-wg-secure-code/topic/symbolic%20execution/near/216345324" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> Dominik Stolz <a href="https://rust-lang.github.io/zulip_archive/stream/146229-wg-secure-code/topic/symbolic.20execution.html#216345324">(Nov 11 2020 at 13:29)</a>:</h4>
<p>Hi! I was wondering if anybody knows why Galois developed <a href="https://github.com/GaloisInc/crucible/tree/master/crux-mir">crux-mir</a> in addition to <a href="https://github.com/GaloisInc/crucible/tree/master/crux-llvm">crux-llvm</a>? What are the benefits of doing symbolic execution on the MIR as opposed to the LLVM IR?</p>



<a name="216345503"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/146229-wg-secure-code/topic/symbolic%20execution/near/216345503" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> oli <a href="https://rust-lang.github.io/zulip_archive/stream/146229-wg-secure-code/topic/symbolic.20execution.html#216345503">(Nov 11 2020 at 13:31)</a>:</h4>
<p>I don't know, but I'd guess it's the fact that there's much more high-level information available</p>



<a name="216345770"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/146229-wg-secure-code/topic/symbolic%20execution/near/216345770" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> Dominik Stolz <a href="https://rust-lang.github.io/zulip_archive/stream/146229-wg-secure-code/topic/symbolic.20execution.html#216345770">(Nov 11 2020 at 13:33)</a>:</h4>
<p>Do you have an example for information only available on the MIR which would be particularly useful for symbolic execution? (type information?)</p>



<a name="216348692"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/146229-wg-secure-code/topic/symbolic%20execution/near/216348692" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> oli <a href="https://rust-lang.github.io/zulip_archive/stream/146229-wg-secure-code/topic/symbolic.20execution.html#216348692">(Nov 11 2020 at 13:57)</a>:</h4>
<p>probably layout information about enums</p>



<a name="216348701"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/146229-wg-secure-code/topic/symbolic%20execution/near/216348701" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> oli <a href="https://rust-lang.github.io/zulip_archive/stream/146229-wg-secure-code/topic/symbolic.20execution.html#216348701">(Nov 11 2020 at 13:58)</a>:</h4>
<p>llvm just sees weird structs</p>



<a name="216350298"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/146229-wg-secure-code/topic/symbolic%20execution/near/216350298" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> scottmcm <a href="https://rust-lang.github.io/zulip_archive/stream/146229-wg-secure-code/topic/symbolic.20execution.html#216350298">(Nov 11 2020 at 14:11)</a>:</h4>
<p>More than just enums -- a <code>struct Foo { a: u32, b: u16, c: u16 }</code> is bitpacked into an LLVM <code>i64</code>, and it's probably easier not to have to deal with all the <a href="https://rust.godbolt.org/z/Pr36Kr">shifts-ands-ors</a> on every field access.</p>



<a name="216352427"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/146229-wg-secure-code/topic/symbolic%20execution/near/216352427" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> Tony Arcieri <a href="https://rust-lang.github.io/zulip_archive/stream/146229-wg-secure-code/topic/symbolic.20execution.html#216352427">(Nov 11 2020 at 14:29)</a>:</h4>
<p><span class="user-mention" data-user-id="302700">@Dominik Stolz</span> if I understand their longer-term plans correctly, they intend to translate MIR to their intermediate language (Crucible)</p>



<a name="216352554"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/146229-wg-secure-code/topic/symbolic%20execution/near/216352554" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> Tony Arcieri <a href="https://rust-lang.github.io/zulip_archive/stream/146229-wg-secure-code/topic/symbolic.20execution.html#216352554">(Nov 11 2020 at 14:30)</a>:</h4>
<p>with Crucible, they can do equivalence proving between implementations in other languages that translate to Crucible, such as Cryptol</p>



<a name="216352818"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/146229-wg-secure-code/topic/symbolic%20execution/near/216352818" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> Tony Arcieri <a href="https://rust-lang.github.io/zulip_archive/stream/146229-wg-secure-code/topic/symbolic.20execution.html#216352818">(Nov 11 2020 at 14:32)</a>:</h4>
<p>that'd be particularly nice for things like <a href="https://github.com/HACS-workshop/hacspec">https://github.com/HACS-workshop/hacspec</a></p>



<a name="216353330"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/146229-wg-secure-code/topic/symbolic%20execution/near/216353330" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> Joshua Nelson <a href="https://rust-lang.github.io/zulip_archive/stream/146229-wg-secure-code/topic/symbolic.20execution.html#216353330">(Nov 11 2020 at 14:36)</a>:</h4>
<p><span class="user-mention" data-user-id="125270">@scottmcm</span> what's the reason for emitting all those bitshifts instead of emitting structs and letting llvm figure it out?</p>



<a name="216353376"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/146229-wg-secure-code/topic/symbolic%20execution/near/216353376" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> Joshua Nelson <a href="https://rust-lang.github.io/zulip_archive/stream/146229-wg-secure-code/topic/symbolic.20execution.html#216353376">(Nov 11 2020 at 14:36)</a>:</h4>
<p>Would be interesting to try that and see if it makes compile times worse or better</p>



<a name="216354058"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/146229-wg-secure-code/topic/symbolic%20execution/near/216354058" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> scottmcm <a href="https://rust-lang.github.io/zulip_archive/stream/146229-wg-secure-code/topic/symbolic.20execution.html#216354058">(Nov 11 2020 at 14:41)</a>:</h4>
<p><span class="user-mention" data-user-id="232545">@Joshua Nelson</span> The shifts are the optimized IR -- looks like we emit stores into an <code>alloca</code> of <code>%Foo = type { [0 x i32], i32, [0 x i16], i16, [0 x i16], i16, [0 x i16] }</code>.  So maybe symbolic on unoptimized LLVM-IR would be ok.  </p>
<p>But if they're doing a lowering to their own IR, starting from MIR is definitely the way to go.  (There are already two backends after MIR, why not a third? <span aria-label="grinning face with smiling eyes" class="emoji emoji-1f601" role="img" title="grinning face with smiling eyes">:grinning_face_with_smiling_eyes:</span>)</p>



<a name="216361842"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/146229-wg-secure-code/topic/symbolic%20execution/near/216361842" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> Tony Arcieri <a href="https://rust-lang.github.io/zulip_archive/stream/146229-wg-secure-code/topic/symbolic.20execution.html#216361842">(Nov 11 2020 at 15:43)</a>:</h4>
<p>whoops, wrong link to hacspec, here's the Rust version: <a href="https://github.com/hacspec/hacspec">https://github.com/hacspec/hacspec</a></p>



<a name="216365434"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/146229-wg-secure-code/topic/symbolic%20execution/near/216365434" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> franziskus <a href="https://rust-lang.github.io/zulip_archive/stream/146229-wg-secure-code/topic/symbolic.20execution.html#216365434">(Nov 11 2020 at 16:10)</a>:</h4>
<p>Right hacspec and crux-mir are supposed to work together in future for equivalence proofs and such.</p>



<hr><p>Last updated: Aug 07 2021 at 22:04 UTC</p>
</html>